\begin{tabbing}
PossibleWorld($D$;$w$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=FairFifo\+
\\[0ex]\& \=($\forall$$i$, $x$:Id. vartype($i$;$x$) $\subseteq\rho$ M($i$).ds($x$))\+
\\[0ex]\& ($\forall$$i$:Id, $a$:Action($i$). $\neg$isnull($a$) $\Rightarrow$ valtype($i$;$a$) $\subseteq\rho$ M($i$).da(kind($a$)))
\\[0ex]\& ($\forall$$l$:IdLnk, ${\it tg}$:Id. ($w$.M($l$,${\it tg}$)) $\subseteq\rho$ M(source($l$)).da(rcv($l$,${\it tg}$)))
\\[0ex]\& ($\forall$$i$, $x$:Id. M($i$).init($x$,s($i$;0).$x$))
\\[0ex]\& (\=$\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]$\neg$isnull(a($i$;$t$))
\\[0ex]$\Rightarrow$ \=(\=islocal(kind(a($i$;$t$)))\+\+
\\[0ex]$\Rightarrow$ M($i$).pre(act(kind(a($i$;$t$))),$\lambda$$x$.s($i$;$t$).$x$,val(a($i$;$t$))))
\-\\[0ex]\& ($\forall$$x$:Id. M($i$).ef(kind(a($i$;$t$)),$x$,$\lambda$$x$.s($i$;$t$).$x$,val(a($i$;$t$)),s($i$;$t$+1).$x$))
\\[0ex]\& (\=$\forall$$l$:IdLnk.\+
\\[0ex]M($i$).send(kind(a($i$;$t$));$l$;$\lambda$$x$.s($i$;$t$).$x$;val(a($i$;$t$));withlnk($l$;m($i$;$t$));$i$))
\-\\[0ex]\& ($\forall$$x$:Id. $\neg$M($i$).frame(kind(a($i$;$t$)) affects $x$) $\Rightarrow$ s($i$;$t$).$x$ $=$ s($i$;$t$+1).$x$)
\\[0ex]\& (\=$\forall$$l$:IdLnk, ${\it tg}$:Id.\+
\\[0ex]$\neg$M($i$).sframe(kind(a($i$;$t$)) sends $<$$l$,${\it tg}$$>$)
\\[0ex]$\Rightarrow$ w{-}tagged(${\it tg}$;onlnk($l$;m($i$;$t$))) $=$ nil))
\-\-\-\\[0ex]\& \=(\=$\forall$$i$, $a$:Id, $t$:$\mathbb{N}$.\+\+
\\[0ex]$\exists$${\it t'}$:$\mathbb{N}$.
\\[0ex]$t$$\leq$${\it t'}$
\\[0ex]\& \=$\neg$isnull(a($i$;${\it t'}$)) \& kind(a($i$;${\it t'}$)) $=$ locl($a$)\+
\\[0ex]$\vee$ $\neg$$a$ declared in M($i$)
\\[0ex]$\vee$ unsolvable M($i$).pre($a$,$\lambda$$x$.s($i$;${\it t'}$).$x$))
\-\-\\[0ex]\& (\=$\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]$\neg$isnull(a($i$;$t$))
\\[0ex]$\Rightarrow$ ($\forall$$x$:Id. $\neg$M($i$).aframe(kind(a($i$;$t$)) affects $x$) $\Rightarrow$ s($i$;$t$).$x$ $=$ s($i$;$t$+1).$x$))
\-\\[0ex]\& ($\forall$$i$, $x$:Id, $k$:Knd. $\neg$M($i$).rframe($k$ reads $x$) $\Rightarrow$ w{-}machine{-}independent($w$;$i$;$k$;$x$))
\\[0ex]\& (\=$\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]$\neg$isnull(a($i$;$t$))
\\[0ex]$\Rightarrow$ ($\forall$$l$:IdLnk. $\neg$M($i$).bframe(kind(a($i$;$t$)) sends on $l$) $\Rightarrow$ onlnk($l$;m($i$;$t$)) $=$ nil))
\-\-\-\-
\end{tabbing}